A:Type, eq:EqDecider(A), P:(AType), f, g:x:A fp Type.
ydom(f). w=f(y)   P(y,w)
 ydom(g). w=g(y)   P(y,w)
 ydom(f  g). w=f  g(y)   P(y,w) 

latex

Definitions	x:A. B(x), , P  Q, xdom(f). v=f(x)   P(x;v), x(s1,s2), Top, t  T, if b then t else f fi , tt, ff, x. t(x), x,y. t(x;y), P  Q, P & Q, , Unit, x(s), P  Q, A, False,
Lemmas	fpf-join-dom2, fpf-join-ap-sq, fpf-dom wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-join wf, top wf, fpf-trivial-subtype-top, fpf-all wf, fpf wf, deq wf